COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	
C00007 00003	 (DEFPROP ITONTOP
C00028 ENDMK
C⊗;

(CSYM AV00) 
(THVSETQ (THV ANS) (LIST (LIST (QUOTE THV) (GENSYM)))) 
(THVSET (CAR (THV ANS)) NIL) 


(THVSETQ (THV WF) NIL) 
(THVSETQ (THV GCTR) 0) 
(THVSETQ (THV ULS) T) 
(THVSETQ (THV UF) NIL) 
(THVSETQ (THV XN) 0) 
(THVSETQ (THV ZN) 0) 
(THVSETQ (THV YN) 0) 
(THVSETQ (THV COMMENTLIST) NIL) 
(THVSETQ (THV PLANL) NIL) 
(THVSETQ (THV ASSL) NIL) 
(THVSETQ (THV PASSUM) NIL) 
(SETQ GTEMP NIL) 
(SETQ CT NIL) 
(SETQ BTSW NIL) 
(THVSETQ (THV DG) NIL) 
(SETQ AL NIL) 
(SETQ AN 0) 
(SETQ SRULES (QUOTE NIL)) 
(SETQ SSW NIL) 
(SETQ FIFOL NIL) 
(SETQ LIFOL NIL) 
(SETQ SN 0) 
(SETQ PN 0) 
(SETQ READY NIL) 
(SETQ UNCERTLIST NIL) 
(THVSETQ (THV DBLITS) NIL) 
(THVSETQ (THV ASSERTLITS) NIL) 
(THVSETQ (THV WASSERTLITS) NIL) 
(SETQ JOINCOND NIL) 
(THVSETQ (THV PROCLIST) NIL) 
(THVSETQ (THV PROCDATA) NIL) 

(THASSERT (AT M L R)) 
(THASSERT (AT B1 L R)) 
(THASSERT (STACKED B3 B2 R)) 
(THASSERT (STACKED B2 B1 R)) 
(THASSERT (BOX B1)) 
(THASSERT (BOX B2)) 
(THASSERT (BOX B4)) 
(THASSERT (STACKED B4 B3 R)) 
(THASSERT (BOX B3)) 
(THASSERT (ROBOT M)) 


(THVSETQ (THV ATARGS) NIL) 
(THVSETQ (THV ATINST) NIL) 

(DEFPROP ATGREMLIN (THERASING (V1 V2) (AT (THV V1) (THV V2) R) (THCOND ((MEMBER (THV ATINST) (THV ATARGS)) (THAS~
SERT (WRONG PATH))))) THEOREM) 

(THASSERT ATGREMLIN) 

(THVSETQ (THV NATARGS) NIL) 
(THVSETQ (THV NATINST) NIL) 

(DEFPROP NATGREMLIN (THERASING (V1 V2) (NAT (THV V1) (THV V2) R) (THCOND ((MEMBER (THV NATINST) (THV NATARGS)) (~
THASSERT (WRONG PATH))))) THEOREM) 

(THASSERT NATGREMLIN) 

(THVSETQ (THV STACKEDARGS) NIL) 
(THVSETQ (THV STACKEDINST) NIL) 

(DEFPROP STACKEDGREMLIN (THERASING (V1 V2) (STACKED (THV V1) (THV V2) R) (THCOND ((MEMBER (THV STACKEDINST) (THV~
 STACKEDARGS)) (THASSERT (WRONG PATH))))) THEOREM) 

(THASSERT STACKEDGREMLIN) 

(THVSETQ (THV NSTACKEDARGS) NIL) 
(THVSETQ (THV NSTACKEDINST) NIL) 

(DEFPROP NSTACKEDGREMLIN (THERASING (V1 V2) (NSTACKED (THV V1) (THV V2) R) (THCOND ((MEMBER (THV NSTACKEDINST) (~
THV NSTACKEDARGS)) (THASSERT (WRONG PATH))))) THEOREM) 

(THASSERT NSTACKEDGREMLIN) 

(THVSETQ (THV ONARGS) NIL) 
(THVSETQ (THV ONINST) NIL) 

(DEFPROP ONGREMLIN (THERASING (V1 V2) (ON (THV V1) (THV V2) R) (THCOND ((MEMBER (THV ONINST) (THV ONARGS)) (THAS~
SERT (WRONG PATH))))) THEOREM) 

(THASSERT ONGREMLIN) 

(THVSETQ (THV NONARGS) NIL) 
(THVSETQ (THV NONINST) NIL) 

(DEFPROP NONGREMLIN (THERASING (V1 V2) (NON (THV V1) (THV V2) R) (THCOND ((MEMBER (THV NONINST) (THV NONARGS)) (~
THASSERT (WRONG PATH))))) THEOREM) 

(THASSERT NONGREMLIN) 

(THVSETQ (THV ONTOPARGS) NIL) 
(THVSETQ (THV ONTOPINST) NIL) 

(DEFPROP ONTOPGREMLIN (THERASING (V1) (ONTOP (THV V1) R) (THCOND ((MEMBER (THV ONTOPINST) (THV ONTOPARGS)) (THAS~
SERT (WRONG PATH))))) THEOREM) 

(THASSERT ONTOPGREMLIN) 

(THVSETQ (THV NONTOPARGS) NIL) 
(THVSETQ (THV NONTOPINST) NIL) 

(DEFPROP NONTOPGREMLIN (THERASING (V1) (NONTOP (THV V1) R) (THCOND ((MEMBER (THV NONTOPINST) (THV NONTOPARGS)) (~
THASSERT (WRONG PATH))))) THEOREM) 

(THASSERT NONTOPGREMLIN) 



(SETQ RTITONTOP NIL) 
(SETQ RFITONTOP NIL) 
 (DEFPROP ITONTOP
	  (THCONSE (X4 X3 X2 X1 FT NT CGL LCTR LWF LUF PS PB BP SASSERTLITS INVAR1 INVAR2 CTST)
		   (ONTOP (THV X1) R)
		   (THSETQ (THV LCTR) (THV GCTR))
		   (SETQ THME (ADD1 THME))
		   (TREEPATH ITONTOP (ONTOP (THV X1) R))
		   (TRACEINFO1)
		   (THOR T (TRACEINFO2 ITONTOP))
		   (COND ((TTYIN) (ADVICESYS)) (T T))
		   (THSETQ (THV LWF) NIL T T)
		   (THCOND ((NOT (THV WF)) (THSETQ (THV LWF) T)) (T T))
		   (THSETQ (THV WF) T)
		   (THSETQ (THV LUF) NIL T T)
		   (THSETQ (THV PS) (EVAL (CAR (THV ANS))) T T)
		   (THSET (CAR (THV ANS)) NIL)
		   (THGOAL (ROBOT (THV X1)))
		   (THGOAL (BOX (THV X2)))
		   (THGOAL (ON (THV X1) (THV X2) R) (THTBF FILTEROP))
		   (THCOND ((THAND (THASVAL (THV X2)) (THASVAL (THV X1)))
			    (THSETQ (THV ONARGS) (CONS (LIST (THV X1) (THV X2)) (THV ONARGS))))
			   (T T))
		   (THCOND ((NULL (THV ONARGS)) T) (T (THSETQ (THV ONARGS) (CDR (THV ONARGS)) T T)))
		   (THSETQ (THV BP) (EVAL (CAR (THV ANS))) T T)
		   (THSET (CAR (THV ANS)) NIL)
		   (THOR T (THFAIL THEOREM))
 		   REP
		   (THGOAL (ROBOT (THV X1)) (THTBF FILTERAX))
		   (THGOAL (BOX (THV X3)) (THTBF FILTERAX))
		   (THGOAL (BOX (THV X4)) (THTBF FILTERAX))
		   (THGOAL (ON (THV X1) (THV X3) R) (THTBF FILTERAX))
		   (THGOAL (STACKED (THV X4) (THV X3) R) (THTBF FILTERAX))
(THSETQ(THV INASS)(LIST(THV X1)(THV X2)(THV X3)(THV X4))T T)
(THSETQ(THV NAMES)(LIST @X1 @X2 @X3 @X4) T T)
(THASSERT(ROBOT Y1))
(THASSERT(BOX Y3))
(THASSERT(BOX Y4))
(THASSERT(ON Y1 Y3 R))
(THASSERT(STACKED Y4 Y3 R))

		   (THSETQ (THV CTST) (QUOTE (ONTOP Y1)))
		   (THOR T (THFAIL THEOREM))
		   (THSETQ (THV SASSERTLITS) (THV ASSERTLITS) T T)
		   (THGOAL (ON Y1 Y4 R) (THTBF FILTEROP))
(PRINT @WHOPEE)(THASSERT(ON(THV X1)(THV X4)R))
(PRINT(THV X1))(PRINT(THV X4))
(THSETQ (THV INVAR1) (QUOTE
   ((ROBOT Z1) (BOX Z3) (BOX Z4) (ON Z1 Z3) (STACKED Z4 Z3))) T T)
		   (THSETQ (THV X4) (QUOTE THUNASSIGNED))
		   (THSETQ (THV X3) (QUOTE THUNASSIGNED))
		   (THGOAL (ROBOT (THV X1)) (THTBF FILTERAX))
		   (THGOAL (BOX (THV X3)) (THTBF FILTERAX))
		   (THGOAL (BOX (THV X4)) (THTBF FILTERAX))
		   (THGOAL (ON (THV X1) (THV X3) R) (THTBF FILTERAX))
		   (THGOAL (STACKED (THV X4) (THV X3) R) (THTBF FILTERAX))
		   (THSETQ (THV PB) (EVAL (CAR (THV ANS))) T T)
		   (SETQ GTEMP
			 (WHILASSEM (THV BP)
				    (THV PB)
				    (CONS (THV NAMES )(THV INASS))
				   (THV INVAR1)
				    (THV CTST)))
		   (THSETQ (THV PB) GTEMP T T)
		   (THSET (CAR (THV ANS)) (APPEND (THV PB) (THV PS)))
		   (THASSERT (ONTOP (THV X1) R))
		   (THCOND ((THV ULS)
			    (THSETQ (THV ASSERTLITS)
				    (CONS (LIST (LIST (QUOTE ONTOP) (THV X1) (QUOTE R)) (LIST (QUOTE A)))
					  (THV ASSERTLITS))))
			   (T
			    (THSETQ (THV WASSERTLITS)
				    (CONS (LIST (LIST (QUOTE ONTOP) (THV X1) (QUOTE R)) (LIST (QUOTE A)))
					  (THV WASSERTLITS)))))
		   (SETQ GANS (REVERSE (EVAL (CAR (THV ANS)))))
		   (THCOND ((THV LWF) (THSETQ (THV WF) NIL T T)
				      (THSETQ (THV BT) NIL T T)
				      (SETQ GANS (REMBT GANS)))
			   (T T))
		   (THSETQ (THV DBLITS) (CONS (CDAR CT) (THV DBLITS)))
		   (THCOND ((THV LUF) (THSETQ (THV UF) NIL T T) (THSETQ (THV ULS) T)) (T T))
		   (THCOND ((THV ULS)
			    (THSETQ (THV ASSERTLITS)
				    (CONS (LIST (LIST (QUOTE ONTOP) (THV X1) (QUOTE R)) (LIST (QUOTE A)))
					  (THV ASSERTLITS))))
			   (T
			    (THSETQ (THV WASSERTLITS)
				    (CONS (LIST (LIST (QUOTE ONTOP) (THV X1) (QUOTE R)) (LIST (QUOTE A)))
					  (THV WASSERTLITS)))))
		   (COND ((EQ (QUOTE IF) (CADAR CT)) (ELSECLAUSE)) (T (THSETQ CT (CDR CT) T T))))
 	  THEOREM)


(SETQ RTSTANDON NIL) 
(SETQ RFSTANDON NIL) 
 (DEFPROP STANDON
	  (THCONSE (CGL Y1 Z1 R1 D1 (LSTSTANDON (QUOTE (Z1 R1))))
		   (ON (THV R1) (THV Z1) R)
		   (THSETQ (THV LCTR) (THV GCTR))
		   (SETQ THME (ADD1 THME))
		   (THUNIQUE LSTSTANDON)
		   (TREEPATH STANDON (ON (THV R1) (THV Z1) R))
		   (TRACEINFO1)
		   (THOR T (TRACEINFO2 STANDON))
		   (COND ((TTYIN) (ADVICESYS)) (T T))
		   (THGOAL (ROBOT (THV R1)))
		   (THGOAL (BOX (THV Z1)))
		   (THGOAL (AT (THV Z1) (THV Y1) R) (THTBF FILTEROP))
		   (THCOND ((THAND (THASVAL (THV Y1)) (THASVAL (THV Z1)))
			    (THSETQ (THV ATARGS) (CONS (LIST (THV Z1) (THV Y1)) (THV ATARGS))))
			   (T T))
		   (THGOAL (AT (THV R1) (THV Y1) R) (THTBF FILTEROP))
		   (THCOND ((THAND (THASVAL (THV Y1)) (THASVAL (THV R1)))
			    (THSETQ (THV ATARGS) (CONS (LIST (THV R1) (THV Y1)) (THV ATARGS))))
			   (T T))
		   (THCOND ((NULL (THV ATARGS)) T) (T (THSETQ (THV ATARGS) (CDR (THV ATARGS)) T T)))
		   (THCOND ((NULL (THV ATARGS)) T) (T (THSETQ (THV ATARGS) (CDR (THV ATARGS)) T T)))
		   (THCOND ((THGOAL (ON (THV R1) (THV D1) R)) (THSETQ (THV ONINST) (LIST (THV R1) (THV D1))))
			   (T T))
		   (THCOND ((THGOAL (ON (THV R1) (THV D1) R))
			    (THERASE (ON (THV R1) (THV D1) R) (THTBF THTRUE)))
			   (T T))
		   (THCOND ((THERASE (WRONG PATH)) (THFAIL THEOREM)) (T T))
		   (THSET (CAR (THV ANS))
			  (CONS (CONS (QUOTE STANDON) (LIST (THV R1) (THV Z1))) (EVAL (CAR (THV ANS)))))
		   (THSETQ (THV DBLITS) (CONS (CDAR CT) (THV DBLITS)))
		   (SETQ THMS (ADD1 THMS))
		   (THASSERT (ON (THV R1) (THV Z1) R))
		   (THCOND ((THV ULS)
			    (THSETQ (THV ASSERTLITS)
				    (CONS (LIST (LIST (QUOTE ON) (THV R1) (THV Z1) (QUOTE R))
						(LIST (QUOTE A) (QUOTE A)))
					  (THV ASSERTLITS))))
			   (T
			    (THSETQ (THV WASSERTLITS)
				    (CONS (LIST (LIST (QUOTE ON) (THV R1) (THV Z1) (QUOTE R))
						(LIST (QUOTE A) (QUOTE A)))
					  (THV WASSERTLITS)))))
		   (PRINT (REVERSE (EVAL (CAR (THV ANS)))))
		   (SETQ GANS (REVERSE (EVAL (CAR (THV ANS)))))
		   (COND ((*GREAT (LENGTH GANS) (LENGTH LGANS)) (SETQ LGANS GANS)) (T T))
		   (THDO (TERPRI))
		   (COND ((EQ (QUOTE IF) (CADAR CT)) (ELSECLAUSE)) (T (THSETQ CT (CDR CT) T T))))
 	  THEOREM)


(SETQ RTSTEPUP NIL) 
(SETQ RFSTEPUP NIL) 
 (DEFPROP STEPUP
	  (THCONSE (CGL Y1 Z1 X1 D1 (LSTSTEPUP (QUOTE (Z1 X1))))
		   (ON (THV X1) (THV Z1) R)
		   (THSETQ (THV LCTR) (THV GCTR))
		   (SETQ THME (ADD1 THME))
		   (THUNIQUE LSTSTEPUP)
		   (TREEPATH STEPUP (ON (THV X1) (THV Z1) R))
		   (TRACEINFO1)
		   (THOR T (TRACEINFO2 STEPUP))
		   (COND ((TTYIN) (ADVICESYS)) (T T))
		   (THGOAL (BOX (THV Y1)))
		   (THGOAL (BOX (THV Z1)))
		   (THGOAL (ROBOT (THV X1)))
		   (THGOAL (STACKED (THV Z1) (THV Y1) R) (THTBF FILTEROP))
		   (THCOND
		    ((THAND (THASVAL (THV Y1)) (THASVAL (THV Z1)))
		     (THSETQ (THV STACKEDARGS) (CONS (LIST (THV Z1) (THV Y1)) (THV STACKEDARGS))))
		    (T T))
		   (THGOAL (ON (THV X1) (THV Y1) R) (THTBF FILTEROP))
		   (THCOND ((THAND (THASVAL (THV Y1)) (THASVAL (THV X1)))
			    (THSETQ (THV ONARGS) (CONS (LIST (THV X1) (THV Y1)) (THV ONARGS))))
			   (T T))
		   (THCOND ((NULL (THV ONARGS)) T) (T (THSETQ (THV ONARGS) (CDR (THV ONARGS)) T T)))
		   (THCOND ((NULL (THV STACKEDARGS)) T)
			   (T (THSETQ (THV STACKEDARGS) (CDR (THV STACKEDARGS)) T T)))
		   (THCOND ((THGOAL (ON (THV X1) (THV D1) R)) (THSETQ (THV ONINST) (LIST (THV X1) (THV D1))))
			   (T T))
		   (THCOND ((THGOAL (ON (THV X1) (THV D1) R))
			    (THERASE (ON (THV X1) (THV D1) R) (THTBF THTRUE)))
			   (T T))
		   (THCOND ((THERASE (WRONG PATH)) (THFAIL THEOREM)) (T T))
		   (THSET (CAR (THV ANS))
			  (CONS (CONS (QUOTE STEPUP) (LIST (THV X1) (THV Y1) (THV Z1)))
				(EVAL (CAR (THV ANS)))))
		   (THSETQ (THV DBLITS) (CONS (CDAR CT) (THV DBLITS)))
		   (SETQ THMS (ADD1 THMS))
		   (THASSERT (ON (THV X1) (THV Z1) R))
		   (THCOND ((THV ULS)
			    (THSETQ (THV ASSERTLITS)
				    (CONS (LIST (LIST (QUOTE ON) (THV X1) (THV Z1) (QUOTE R))
						(LIST (QUOTE A) (QUOTE A)))
					  (THV ASSERTLITS))))
			   (T
			    (THSETQ (THV WASSERTLITS)
				    (CONS (LIST (LIST (QUOTE ON) (THV X1) (THV Z1) (QUOTE R))
						(LIST (QUOTE A) (QUOTE A)))
					  (THV WASSERTLITS)))))
		   (PRINT (REVERSE (EVAL (CAR (THV ANS)))))
		   (SETQ GANS (REVERSE (EVAL (CAR (THV ANS)))))
		   (COND ((*GREAT (LENGTH GANS) (LENGTH LGANS)) (SETQ LGANS GANS)) (T T))
		   (THDO (TERPRI))
		   (COND ((EQ (QUOTE IF) (CADAR CT)) (ELSECLAUSE)) (T (THSETQ CT (CDR CT) T T))))
 	  THEOREM)


(SETQ RTAONTOP NIL) 
(SETQ RFAONTOP NIL) 
 (DEFPROP AONTOP
	  (THCONSE (CGL X2 X3 X1 (LSTAONTOP (QUOTE (X1))))
		   (ONTOP (THV X1) R)
		   (THSETQ (THV LCTR) (THV GCTR))
		   (SETQ THME (ADD1 THME))
		   (THUNIQUE LSTAONTOP)
		   (TREEPATH AONTOP (ONTOP (THV X1) R))
		   (TRACEINFO1)
		   (THOR T (TRACEINFO2 AONTOP))
		   (COND ((TTYIN) (ADVICESYS)) (T T))
		   (THGOAL (BOX (THV X3)))
		   (THGOAL (BOX (THV X2)))
		   (THGOAL (ROBOT (THV X1)))
		   (THGOAL (ON (THV X1) (THV X2) R) (THTBF FILTEROP))
		   (THCOND ((THNOT (THGOAL (STACKED (THV X3) (THV X2) R))) T)
			   (T (THGOAL (NSTACKED (THV X3) (THV X2) R) (THTBF FILTEROP))))
		   (THSETQ (THV DBLITS) (CONS (CDAR CT) (THV DBLITS)))
		   (SETQ THMS (ADD1 THMS))
		   (COND ((EQ (QUOTE IF) (CADAR CT)) (ELSECLAUSE)) (T (THSETQ CT (CDR CT) T T))))
 	  THEOREM)

(THASSERT AONTOP) 

(THASSERT STEPUP) 

(THASSERT STANDON) 

(THASSERT ITONTOP) 

 (DEFPROP RESTOREPROP
	  (LAMBDA NIL
	   (PROG NIL
		 (SETQ STAT T)
		 (SETQ FUNDEFLIST (QUOTE NIL))
		 (PUTPROP (QUOTE ON) T (QUOTE DEF))
		 (PUTPROP (QUOTE ON) (QUOTE (X *)) (QUOTE UNIQ))
		 (PUTPROP (QUOTE ON) (QUOTE NIL) (QUOTE UNCERT))
		 (PUTPROP (QUOTE ON) (QUOTE NIL) (QUOTE PARTIAL))
		 (PUTPROP (QUOTE ON) (QUOTE T) (QUOTE FLUENT))
		 (PUTPROP (QUOTE ONTOP) T (QUOTE DEF))
		 (PUTPROP (QUOTE ONTOP) (QUOTE NIL) (QUOTE UNIQ))
		 (PUTPROP (QUOTE ONTOP) (QUOTE NIL) (QUOTE UNCERT))
		 (PUTPROP (QUOTE ONTOP) (QUOTE NIL) (QUOTE PARTIAL))
		 (PUTPROP (QUOTE ONTOP) (QUOTE T) (QUOTE FLUENT))
		 (PUTPROP (QUOTE BOX) T (QUOTE DEF))
		 (PUTPROP (QUOTE BOX) (QUOTE NIL) (QUOTE UNIQ))
		 (PUTPROP (QUOTE BOX) (QUOTE NIL) (QUOTE UNCERT))
		 (PUTPROP (QUOTE BOX) (QUOTE NIL) (QUOTE PARTIAL))
		 (PUTPROP (QUOTE BOX) (QUOTE NIL) (QUOTE FLUENT))
		 (PUTPROP (QUOTE STACKED) T (QUOTE DEF))
		 (PUTPROP (QUOTE STACKED) (QUOTE (X *)) (QUOTE UNIQ))
		 (PUTPROP (QUOTE STACKED) (QUOTE NIL) (QUOTE UNCERT))
		 (PUTPROP (QUOTE STACKED) (QUOTE NIL) (QUOTE PARTIAL))
		 (PUTPROP (QUOTE STACKED) (QUOTE T) (QUOTE FLUENT))
		 (PUTPROP (QUOTE AT) T (QUOTE DEF))
		 (PUTPROP (QUOTE AT) (QUOTE (X *)) (QUOTE UNIQ))
		 (PUTPROP (QUOTE AT) (QUOTE NIL) (QUOTE UNCERT))
		 (PUTPROP (QUOTE AT) (QUOTE NIL) (QUOTE PARTIAL))
		 (PUTPROP (QUOTE AT) (QUOTE T) (QUOTE FLUENT))
		 (PUTPROP (QUOTE ROBOT) T (QUOTE DEF))
		 (PUTPROP (QUOTE ROBOT) (QUOTE NIL) (QUOTE UNIQ))
		 (PUTPROP (QUOTE ROBOT) (QUOTE NIL) (QUOTE UNCERT))
		 (PUTPROP (QUOTE ROBOT) (QUOTE NIL) (QUOTE PARTIAL))
		 (PUTPROP (QUOTE ROBOT) (QUOTE NIL) (QUOTE FLUENT))
		 (PUTPROP (QUOTE ITONTOP) (QUOTE NIL) (QUOTE INEQ))
		 (PUTPROP (QUOTE ITONTOP) (QUOTE NIL) (QUOTE REC))
		 (PUTPROP (QUOTE ITONTOP) (QUOTE NIL) (QUOTE ASSUM))
		 (PUTPROP (QUOTE ITONTOP) (QUOTE NIL) (QUOTE ARG))
		 (PUTPROP (QUOTE ITONTOP) T (QUOTE ITER))
		 (PUTPROP (QUOTE STEPUP) (QUOTE NIL) (QUOTE INEQ))
		 (PUTPROP (QUOTE STEPUP) (QUOTE NIL) (QUOTE REC))
		 (PUTPROP (QUOTE STEPUP) (QUOTE NIL) (QUOTE ASSUM))
		 (PUTPROP (QUOTE STEPUP) (QUOTE (X1 Y1 Z1)) (QUOTE ARG))
		 (PUTPROP (QUOTE STEPUP) T (QUOTE OP))
		 (PUTPROP (QUOTE STANDON) (QUOTE NIL) (QUOTE INEQ))
		 (PUTPROP (QUOTE STANDON) (QUOTE NIL) (QUOTE REC))
		 (PUTPROP (QUOTE STANDON) (QUOTE NIL) (QUOTE ASSUM))
		 (PUTPROP (QUOTE STANDON) (QUOTE (R1 Z1)) (QUOTE ARG))
		 (PUTPROP (QUOTE STANDON) T (QUOTE OP))
		 (PUTPROP (QUOTE AONTOP) (QUOTE NIL) (QUOTE INEQ))
		 (PUTPROP (QUOTE AONTOP) (QUOTE NIL) (QUOTE REC))
		 (PUTPROP (QUOTE AONTOP) (QUOTE NIL) (QUOTE ASSUM))
		 (PUTPROP (QUOTE AONTOP) (QUOTE NIL) (QUOTE ARG))
		 (PUTPROP (QUOTE AONTOP) T (QUOTE AX))))
 	  EXPR)